day 5 - Sudo Sudoko

Santa's little helpers are notoriously good at solving Sudoku puzzles.
Because regular Sudoku puzzles are too trivial, they have invented a variant.

    1 2 3   4 5 6   7 8 9
  +-------+-------+-------+
A | . . . | . . . | . . 1 |
B | . 1 2 | . . . | . . . |
C | . . . | . . . | 2 . . |
  +-------+-------+-------+
D | . . . | . . . | . . 2 |
E | . 2 . | . . . | . . . |
F | . . . | . . . | . . . |
  +-------+-------+-------+
G | . . . | . . . | 1 2 . |
H | 1 . . | . . 2 | . . . |
I | . . . | 1 . . | . . . |
  +-------+-------+-------+

In addition to the standard Sudoku puzzle above,
the following equations must also hold:

B9 + B8 + C1 + H4 + H4 = 23
A5 + D7 + I5 + G8 + B3 + A5 = 19
I2 + I3 + F2 + E9 = 15
I7 + H8 + C2 + D9 = 26
I6 + A5 + I3 + B8 + C3 = 20
I7 + D9 + B6 + A8 + A3 + C4 = 27
C7 + H9 + I7 + B2 + H8 + G3 = 31
D3 + I8 + A4 + I6 = 27
F5 + B8 + F8 + I7 + F1 = 33
A2 + A8 + D7 + E4 = 21
C1 + I4 + C2 + I1 + A4 = 20
F8 + C1 + F6 + D3 + B6 = 25

If you then read the numbers clockwise starting from A1 to A9, to I9, to I1 and
back to A1, you end up with a number with 32 digits.  Enclose that in AOTW{...}
to get the flag.

diff --git a/sudoku-z3.py b/sudoku-z3.py
old mode 100755
new mode 100644
index 4e15087..9a1a2fa
--- a/sudoku-z3.py
+++ b/sudoku-z3.py
@@ -100,6 +100,19 @@ def Z3Solving(sudoku):
         for j in range(3):
             s.add(Distinct([symbols["ABCDEFGHI"[m + i * 3] + "123456789"[n + j * 3]] for m in range(3) for n in range(3)]))

+    s.add((symbols["B9"] + symbols["B8"] + symbols["C1"] + symbols["H4"] + symbols["H4"]) == 23)
+    s.add((symbols["A5"] + symbols["D7"] + symbols["I5"] + symbols["G8"] + symbols["B3"] + symbols["A5"]) == 19)
+    s.add((symbols["I2"] + symbols["I3"] + symbols["F2"] + symbols["E9"]) == 15)
+    s.add((symbols["I7"] + symbols["H8"] + symbols["C2"] + symbols["D9"]) == 26)
+    s.add((symbols["I6"] + symbols["A5"] + symbols["I3"] + symbols["B8"] + symbols["C3"]) == 20)
+    s.add((symbols["I7"] + symbols["D9"] + symbols["B6"] + symbols["A8"] + symbols["A3"] + symbols["C4"]) == 27)
+    s.add((symbols["C7"] + symbols["H9"] + symbols["I7"] + symbols["B2"] + symbols["H8"] + symbols["G3"]) == 31)
+    s.add((symbols["D3"] + symbols["I8"] + symbols["A4"] + symbols["I6"]) == 27)
+    s.add((symbols["F5"] + symbols["B8"] + symbols["F8"] + symbols["I7"] + symbols["F1"]) == 33)
+    s.add((symbols["A2"] + symbols["A8"] + symbols["D7"] + symbols["E4"]) == 21)
+    s.add((symbols["C1"] + symbols["I4"] + symbols["C2"] + symbols["I1"] + symbols["A4"]) == 20)
+    s.add((symbols["F8"] + symbols["C1"] + symbols["F6"] + symbols["D3"] + symbols["B6"]) == 25)
+
     # now we put the assumptions of the given puzzle into the solver:
     for elem, value in sudoku.values.items():
         if value in "123456789":
@@ -128,7 +141,7 @@ if __name__ == "__main__":

     if len(argv) != 2:
         print("[!] we are using some test puzzle due to missing argument")
-        main("4.....8.5.3..........7......2.....6.....8.4......1.......6.3.7.5..2.....1.4......")
+        main("........1.12............2..........2.2......................12.1....2......1.....")
     else:
         main(argv[1])